Nuprl Lemma : m-sys-sub-join-map 0,22
T:Type, L:T List, f:(TSystem), x:T.
(x,yL.f(x) || f(y))  (x  L)  f(x)  (map(x.f(x);L)) 
latex

Definitionsx,y. t(x;y), D1  D2, P  Q, P  Q, P  Q, x:A. B(x), P & Q, (x  l), Prop, t  T, (x,yL.P(x;y)), A || B, map(f;as), x(s), x:A. B(x), Feasible(M), MsgA, Id, System, Dsys
Lemmasl member wf, ma-feasible wf, msga wf, Id wf, dsys wf, member map, msystem wf, map wf, m-sys-sub-join-list, m-sys-compatible wf, pairwise wf, pairwise-map

origin